package operateurs;

import utils.FormuleType;
import utils.Symbole;
import base.Formule;

/**
 * Created by IntelliJ IDEA.
 * User: njussien
 * Date: 30/11/12
 * Time: 10:38
 */
public class Implique extends OperateurBinaire {
    public Implique(Formule a, Formule b) {
    	this.operande = a;
    	this.operandedroit = b;
    }
    
    public String toString() {
    	//return "(" + this.operande + " → " + this.operandedroit + ")";
    	return "(" + this.operande + " " + Symbole.IMPLIQUE + " " + this.operandedroit + ")";
    }

	public Formule supprimeConnecteurs() {
		return new Ou(this.operande.negation(), this.operandedroit);
	}
	
	public Formule negation() {
		return new Et(this.operande, this.operandedroit.negation());
	}
	
	/**
	 * S'il reste une implication lors du transport de la negation, il y a un problème d'implementation
	 */
	public Formule descendreNegation(boolean isNegatif) {
		throw new UnsupportedOperationException();
	}

	public Formule transportQuantificateurs() {
		return new Implique(this.operande.transportQuantificateurs(), this.operandedroit.transportQuantificateurs());
	}
	
	public boolean isSame(Formule o) {
		//if (o.getType() != FormuleType.IMPLIQUE) return false;
		if (o.getClass() != Implique.class) return false;
		Implique tmp = (Implique)o;
		return this.operande.isSame(tmp.operande) && this.operandedroit.isSame(tmp.operandedroit);
	}

	public Formule miseFormeClausale() {
		// TODO
		return new Implique(this.operande.miseFormeClausale(), this.operandedroit.miseFormeClausale());
	}

	public FormuleType getType() {
		return FormuleType.IMPLIQUE;
	}

	public boolean isQuantifieursInOrder(boolean aUniversel) {
		throw new UnsupportedOperationException();
	}
}
